the_es:ES, e', e:E.
(e  before(e'))  (l:E List. (before(e') = (before(e) @ [e] @ l)  (E List))) 

latex

Definitions	x:A. B(x), P  Q, x:A. B(x), t  T, T, True, , Top, S  T, ||as||, P  Q, P  Q, P & Q, i  j , t  ...$L, Y, A  B, A, False, l[i], hd(l), nth_tl(n;as), if b then t else f fi , i z j, b, i <z j, tt, ff
Lemmas	l member decomp, append wf, squash wf, true wf, es-before wf, l member wf, es-E wf, event system wf, firstn-before, length wf nat, top wf, length wf1, length append, add functionality wrt eq, length nil, non neg length, length cons, firstn wf, firstn append, firstn length, select wf, select append back, select append front, le wf